Notes (Week 10 Tuesday)

Scheduler
=========

If we don't know anything about a scheduler, we assume it can choose
whatever interleavings between processes it wants, for example:

x-x-x-x-x-x-x-x

y-y-y-y-y-y-y-y

x-x-x-    x-x-x
      y-y-

x-  x-  x-  x-
  y-  y-  y-  y

etc.


Session Types
=============

Choice and selection
--------------------

// Server process: providing *choice*

serve_eat_here |- Δ, x : SEatHere
                                 serve_takeaway |- Δ, x : STakeAway
------------------------------------------------------------------ &
x.case(serve_eat_here,serve_takeaway) |- Δ, x : SEatHere & STakeAway

SEatHere = dual(EatHere)
STakeAway = dual(TakeAway)
SEatHere & STakeAway = dual(EatHere (+) TakeAway)


// Customer process: making *selection*

// Selection 1: send choice "eat here" then wait for food 

         eat_here |- Γ, x : EatHere
---------------------------------------------- (+)1
x[inl].eat_here |- Γ, x : EatHere (+) TakeAway

EatHere = dual(SEatHere)
TakeAway = dual(STakeAway)
EatHere (+) TakeAway = dual(SEatHere & STakeAway)

// Selection 2: send choice "takeaway" then wait for takeaway

         takeaway |- Γ, x : TakeAway
---------------------------------------------- (+)2
x[inr].takeaway |- Γ, x : EatHere (+) TakeAway


// Dynamic Semantics of Choice/Selection

Run 1: left choice
ch x. x[inl].eat_here | x.case(serve_eat_here,serve_takeaway)
==> ch x. (eat_here | serve_eat_here)

Run 2: right choice
ch x. [inr].takeaway | x.case(serve_eat_here,serve_takeaway)
==> ch x. (takeaway | serve_takeaway)


Input and output (incl. empty input/output)
-------------------------------------------

// Customer process
x[y].(pay | x(z).x().get_receipt)

// Customer process typing derivation

                          get_receipt |- y:GetReceipt
                     ----------------------------------- ⊥
                     x().get_receipt |- y:GetReceipt,x:⊥
                  ----------------------------------------- ⅋
pay |- y : Pay    x(z).x().get_receipt |- x: GetReceipt ⅋ ⊥
--------------------------------------------------------------- (x)
x[y].(pay | x(z).x().get_receipt) |- x: Pay (x) (GetReceipt ⅋ ⊥)


// Server process
x(y).x[z].(give_receipt | x[].0)

// Server process typing derivation

Having derived the customer process type, we figured out what the
server process' type ought to be by taking its dual:

dual (GetReceipt ⅋ ⊥) = dual(GetReceipt) (x) 1
x(y).x[z].(give_receipt | x[].0) |- x: dual(Pay) ⅋ (dual(getReceipt) (x) 1)

But constructing the typing derivation tree makes sure of it:

                                                    ------------ 1
    give_receipt |- y:dual(Pay),z:GiveReceipt       x[].0 |- x:1
   --------------------------------------------------------------- (x)
   x[z].(give_receipt | x[].0) |- y:dual(Pay), x:(GiveReceipt (x) 1)
 ------------------------------------------------------------------- ⅋
 x(y).x[z].(give_receipt | x[].0) |- dual(Pay) ⅋ (GiveReceipt (x) 1)


// Dynamic Semantics of Input/Output

// Relevant reduction/equivalence rules
ch x. (x[y].(P | Q) | x(y).R) ==> ch y. (P | ch x. (Q | R))  "beta-(x)⅋"
ch x. (x[].0 | x().P) ==> P  "beta-1⊥"
ch x:A. (P | Q) == ch x:dual(A).(Q | P)  "swap"

                  Customer                      Server
ch x. (x[y].(pay | x(z).x().get_receipt) | x(y).x[z].(give_receipt | x[].0))
==> "beta-(x)⅋"
ch y. (pay | ch x. (x(z).x().get_receipt | x[z].(give_receipt | x[].0)))
==> "swap"
ch y. (pay | ch x. (x[z].(give_receipt | x[].0)) | x(z).x().get_receipt)
==> "beta-(x)⅋"
ch y. (pay | ch z. (give_receipt | ch x. (x[].0 | x().get_receipt)))
==> "beta-1⊥"
ch y. (pay | ch z. (give_receipt | get_receipt))


Deadlock freedom of Session Types
---------------------------------

  P |- Γ, x : A      Q |- Δ, x : dual(A)
  -------------------------------------- Cut
         ch x:A. (P | Q) |- Γ, Δ 

- Absence of communication loops between P and Q.

- Wadler: "Communications along Γ and Δ are disjoint, so P and Q are
  restricted to communicate with each other only along x. If communication
  could occur along two channels rather than one, then one could form a
  loop of communications between P and Q that leads to deadlock."

- Examples of deadlock-prone concurrent processes:

    ch x. (x(u).wait_meal | x(v).wait_payment)
      - won't type check, because their types for x aren't dual

    ch x, y. (x(u).wait_meal | y(v).wait_payment)
      - also won't type check, because we can't introduce ch for
        two channels at once

- These would be rejected by session types, because Cut is the only typing
  rule to introduce a `ch` binder when typechecking parallel composition
  of two well-typed processes, and (1) their types for the one channel must
  be dual, and (2) Cut does not allow you to bind more than one channel
  simultaneously for these processes to communicate by:

  ---------------------------------------------------------------- Cut? no.
  ch x:A⅋C. ch y:B⅋D. (x(u).wait_meal | y(v).wait_payment) |- Γ, Δ 



What if you *wanted* to express systems that allow deadlock?
------------------------------------------------------------

- An additional rule "Binary Cut allows one to express systems where
  communications form a loop and may deadlock"

    P |- Γ, x : A, y : B      Q |- Δ, x : dual(A), y : dual(B)
    ---------------------------------------------------------- BiCut
                ch x:A, y:B. (P | Q) |- Γ, Δ 

- The deadlock-prone example would be accepted by session types with BiCut

     R |- Θ, y : A, x : B 
    ---------------------- ⅋
    x(y).R |- Θ, x : A ⅋ B

(NB: Remember, order in session typing environments is ignored)

          etc.                                  etc.
----------------------------  ---------------------------------------------
wait_meal |- Γ,u:A,x:C,y:B⅋D  wait_pay |- Δ,x:dual(A⅋C),v:dual(B),y:dual(D)
----------------------------  ---------------------------------------------
x(u).wait_meal |- Γ,x:A⅋C,y:B⅋D  y(v).wait_pay |- Δ,x:dual(A⅋C),y:dual(B⅋D)
---------------------------------------------------------------------------
      ch x:A⅋C,y:B⅋D. (x(u).wait_meal | y(v).wait_pay) |- Γ, Δ 


Final Exam
==========

- Online with a login (we'll give you credentials)

- 2 hours within a 4 hour window (last year)

- Open book, but no active seeking of answers (via online interactions etc)